\documentclass{beamer}
\usetheme{Darmstadt}
\usecolortheme{beaver}
\usepackage{listings}
\usepackage[utf8]{inputenc}
\usepackage[french]{babel}
\PassOptionsToPackage{usenames,dvipsnames}{xcolor}
\usepackage{colortbl,verbatim}
\usepackage{algpseudocode}
\usepackage{algorithm}
\usepackage{alltt}
\usepackage{graphics}

\definecolor{whiteblue}{RGB}{154,192,205}


\begin{document}

\author{David \textsc{Declerck} \& Rémy \textsc{El Sibaïe Besognet}}
\title{Vérification de programmes à l'Algony}
\date{\today}

\begin{frame}
  \titlepage
\end{frame}

\begin{frame}{Introduction}
\begin{itemize}
\item Contexte : la {\color{blue}\emph{programmation concurrente}}
\item Concepts vus en cours (algorithmique répartie, systèmes, architecture)
\item Exemple : ordonnanceurs des systèmes d'exploitation, protocoles
  de cohérence de cache des microprocesseurs\dots
\item Ecriture de programmes concurrents difficile
  %% La littérature regorge d'algo concurrents, leur écriture n'est
  %% pas triviale
\item Objectif : s'assurer que ces algorithmes soient {\color{blue}\emph{corrects}}
\end{itemize}
\end{frame}

\begin{frame}{Propriétés à vérifier}
\begin{itemize}
\item {\color<2>{red}{sûreté (safety)}}
\item \color<2>{gray}vivacité (liveness)
\item équité (fairness)
\item absence d'interblocages (deadlock-freeness)
\end{itemize}
\end{frame}



\begin{frame}{Vérification de programmes}
\begin{itemize}
\item Vérification {\color{blue}\emph{formelle}} (pas de tests)
\item Vérification {\color{blue}\emph{automatique}}
  %% on donne un programme, on appuie sur un bouton
  %% et ça nous dit, ça marche ou pas
\item On vérifie un modèle de programme
\item Un programme = un système de transitions
\end{itemize}
\end{frame}

\begin{frame}{Système de transitions}
\centering
\includegraphics[scale=0.3]{autom.png}
\medskip
\onslide<2>
\begin{columns}
\begin{column}{4cm}
\centering
programme\\
$=$\\
système de transitions
\end{column}
\begin{column}{2cm}
donc
\end{column}
\begin{column}{4cm}
\centering
sûreté\\
$=$\\
atteignabilité d'un état dangereux
\end{column}
\end{columns}
\end{frame}

\begin{frame}{Vérification des programmes parallèles}
\begin{itemize}
\item Plusieurs processus ou threads en parallèle
\item En réalité, équivaut à un {\color{blue}\emph{problème séquentiel}} (entrelacement)
\item Ordre des transitions arbitraire (ordonnanceur inconnu)\\
$\rightarrow$ Explosion combinatoire : $e^n$ etats
%% c'est ce qu'on appelle le model checking
\end{itemize}
\medskip
\onslide<2>
\begin{center}
\includegraphics[scale=0.3]{explosion.png}
\end{center}
\end{frame}


\begin{frame}{Model Checking : deux approches}
\begin{itemize}
\item Enumerated model Checking
\item Généralisation à n processus
\end{itemize}
\medskip
$\rightarrow$ Logiciel utilisé : {\color{red}\emph{Cubicle}}

\end{frame}

\begin{frame}[fragile]{Exemple : algorithme de Peterson}
\footnotesize
\begin{columns}
\begin{column}{5cm}
\begin{alltt}P0: flag[0] = true;
    turn = 1;
    \textcolor{blue}{while} (flag[1] == true
        && turn == 1)
    \{
        // busy wait
    \}
    // critical section

    // end of critical section
    flag[0] = false;
\end{alltt}
\end{column}
\begin{column}{5cm}
\begin{alltt}	
P1: flag[1] = true;
    turn = 0;
    \textcolor{blue}{while} (flag[0] == true
        && turn == 0)
    \{
        // busy wait
    \}
    // critical section

    // end of critical section
    flag[1] = false;
\end{alltt}
\end{column}
\end{columns}
\end{frame}


\begin{frame}[fragile]{Exemple : algorithme de Szymanski}
\begin{algorithmic}[1]
\State $Bx\gets true$
\State \textbf{await} $\forall y$ . $x \neq y \Rightarrow not\
Sy$ \textbf{then} $Bx \gets false$
\State $Wx \gets true$; $Sx \gets true$;

\If {$\exists y$ . $x \neq y \Rightarrow not\ By \wedge not\ Wy$}
    \State $Sx \gets false$; $goto\ 9$
\Else
    \State $Wx \gets false$; $goto\ 10$
\EndIf
\State \textbf{await} $\exists y$ . $x \neq y \Rightarrow Sy \vee not\
Wx$ \textbf{then} $Wx \gets false$ ; $Sx \gets true$;
\State \textbf{await} $\forall y$ . $x \neq y \Rightarrow not\ Wy$
\State \textbf{await} $\forall y$ . $y < x \Rightarrow not\ Sy$
\State \{Critical Section\} 
\State $Sx\gets false$; $goto\ 1$
\end{algorithmic}
\end{frame}


\begin{frame}[fragile]{Szymanski en Cubicle : ça pique les yeux\dots}
\tiny
\begin{columns}
\begin{column}{5cm}
\begin{verbatim}
type location = L0 | L1 | L2 | L3 | L4 | L5 | L6 | L7 

array A[proc] : location
array B[proc] : bool
array S[proc] : bool
array W[proc] : bool 

init (x) { A[x] = L0 && S[x] = False &&
           W[x] = False && B[x] = False }
 
unsafe (z1 z2) { A[z1] = L7 && A[z2] = L7 }

transition t0 (x)
requires { A[x] = L0 }
{ A[x] := L1; B[x] := True }

transition t1 (x)
requires { A[x] = L1 && forall_other y.
           S[y] = False }
{ A[x] := L2; B[x] := False }

transition t2 (x)
requires { A[x] = L2 }
{ A[x] := L3; S[x] := True; W[x] := True }

transition t3_then (x y)
requires { A[x] = L3 && B[y] = False &&
           W[y] = False }
{ A[x] := L4; S[x] := False }
\end{verbatim}
\end{column}
\begin{column}{5cm}
\begin{verbatim}
transition t3_else (x)
requires { A[x] = L3 && forall_other y.
           ( B[y] =  True || W[y] = True ) }
{ A[x] := L5; W[x] := False }

transition t4 (x y)
requires { A[x] = L4 && S[y] = True &&
           W[y] = False }
{ A[x] := L5; S[x] := True; W[x] := False }

transition t5 (x)
requires { A[x] = L5 && forall_other y.
           W[y] = False }
{ A[x] := L6 }

transition t6 (x)
requires { A[x] = L6 && forall_other j.
           (x <= j || S[j] = False) }
{ A[x] := L7 }

transition t7 (x)
requires { A[x] = L7 }
{ A[x] := L0; S[x] := False }
\end{verbatim}
\end{column}
\end{columns}
\end{frame}


\begin{frame}{Problématique du TER}
Simplifier l'écriture d'algorithmes sous Cubicle en\dots
\begin{itemize}
\item Concevant un langage : Algony
\item Créant un {\color{blue}compilateur} d'Algony vers Cubicle\\
      (grâce aux connaissances acquises en compilation)
\end{itemize}
\medskip
Fonctionnalités souhaitées : affectation, boucle, instruction
conditionnelle, tableaux, section critique, attente active
\end{frame}

\begin{frame}[fragile]{Szymanski à l'Algony}
\scriptsize
\begin{columns}
\begin{column}{4cm}
\begin{verbatim}
array B[proc] : bool 
array S[proc] : bool 
array W[proc] : bool 

current x 

while true do //L1
  B[x] := true //L2
  await forall_other y . //L3
    S[y] = false then
    atomic
      B[x] := false
      W[x] := true
      S[x] := true
    end
\end{verbatim}
\end{column}
\begin{column}{5cm}
\begin{verbatim}
  if exists_other y . //L4
    B[y] = false && W[y] = false then
    S[x] := false //L5
    await exists_other y . //L6
      S[y] = true && W[y] = false then
      atomic //L7
        W[x] := false
        S[x] := true
      end
  else
    W[x] := false //L8
  endif 
  await forall_other y . //L9
    W[y] = false
  await forall_other y . //L10
    y >= x || S[y] = false 
  critical //Enter critical section
  S[x] := false 
done
\end{verbatim}
\end{column}
\end{columns}
\end{frame}



\begin{frame}[fragile]{Cubicle : le langage cible}

 Des transitions :
{\footnotesize
\begin{verbatim}
transition t (p1 p2)
requires { Tab[p1] = True && Tab[p2] = False &&
           forall_other p3. (Tab[p3] = False) }
{
    Tab[p1] = False;
    Tab[p2] = True
}
\end{verbatim}
}

Un état initial :
{\footnotesize
\begin{verbatim}
init (p) { Tab[p] = False && Var = 1 }
\end{verbatim}
}

Des états dangereux:
{\footnotesize
\begin{verbatim}
unsafe (p1 p2) { Tab[p1] = True && Tab[p2] = True }
\end{verbatim}
}

\end{frame}



\begin{frame}{}
\begin{center}
\LARGE Comment traduire ?
\end{center}
\end{frame}



\begin{frame}[fragile]{Traduction : principe général}

\begin{itemize}
\item Introduction d'un compteur d'instructions
\begin{verbatim}
type location = L1 | L2 | L3 | L4...
array PC [proc] : location

\end{verbatim}
\item<2,3,4> Etat initial
\begin{verbatim}
init (p) { PC[p] = L1 }

\end{verbatim}
\item<3,4> Des transitions
\begin{alltt}
transition t (p)
requires \{ PC[p] = L1 && \textcolor{red}{<cond>} \}
\{ <instr> ; PC[p] = L2 \}

\end{alltt}
\item<4> Présentation de quelques instructions
\end{itemize}
\end{frame}



\begin{frame}[fragile]{Traduction : Instruction While}

\begin{columns}[c]
\begin{column}{4cm}
\footnotesize
\begin{alltt}
while <cond> do (* \textcolor{magenta}{L1} *)
  <instr> (* \textcolor{green}{L2} *)
done (* \textcolor{blue}{L3} *)
(* \textcolor{orange}{L4} *)
\end{alltt}
\centering
\onslide<2,3>
\includegraphics[scale=0.35]{while.png}
\end{column}
\onslide<3>
\begin{column}{0.5cm}
$\rightarrow$
\end{column}
\begin{column}{5cm}
\footnotesize
\begin{alltt}
transition while_true (p)
requires \{ PC[p] = \textcolor{magenta}{L1} && \textcolor{red}{<cond>} \}
\{ PC[p] = \textcolor{green}{L2} \}

transition while_false (p)
requires \{ PC[p] = \textcolor{magenta}{L1} && \textcolor{red}{<!cond>} \}
\{ PC[p] = \textcolor{orange}{L4} \}

transition stmt (p)
requires \{ PC[p] = \textcolor{green}{L2} \}
\{ <instr> ; PC[p] = \textcolor{blue}{L3} \}

transition while_loop (p)
requires \{ PC[p] = \textcolor{blue}{L3} \}
\{ PC[p] = \textcolor{magenta}{L1} \}
\end{alltt}
\end{column}
\end{columns}
\end{frame}


\begin{frame}[fragile]{Traduction : Instruction If}

\begin{columns}[c]
\begin{column}{4cm}
\footnotesize
\begin{alltt}
if <cond> then (* \textcolor{magenta}{L1} *)
  <instr> (* \textcolor{green}{L2} *)
else
  <instr> (* \textcolor{blue}{L3} *)
endif
(* \textcolor{orange}{L4} *)  
\end{alltt}
\centering
\onslide<2,3>
\includegraphics[scale=0.35]{if.png}
\end{column}
\onslide<3>
\begin{column}{0.5cm}
$\rightarrow$
\end{column}
\begin{column}{5cm}
\footnotesize
\begin{alltt}
transition if_true (p)
requires \{ PC[p] = \textcolor{magenta}{L1} && \textcolor{red}{<cond>} \}
\{ PC[p] = \textcolor{green}{L2} \}

transition if_false (p)
requires \{ PC[p] = \textcolor{magenta}{L1} && \textcolor{red}{<!cond>} \}
\{ PC[p] = \textcolor{blue}{L3} \}

transition true_stmt (p)
requires \{ PC[p] = \textcolor{green}{L2} \}
\{ <instr> ; PC[p] = \textcolor{orange}{L4} \}

transition false_stmt (p)
requires \{ PC[p] = \textcolor{blue}{L3} \}
\{ <instr> ; PC[p] = \textcolor{orange}{L4} \}
\end{alltt}
\end{column}
\end{columns}
\end{frame}


\begin{frame}[fragile]{Traduction : Instruction Critical}

\begin{columns}[c]
\begin{column}{3cm}
\footnotesize
\begin{alltt}
critical (* \textcolor{magenta}{L1} *)
(* \textcolor{green}{L2} *)
\end{alltt}
\end{column}
\begin{column}{1cm}
$\rightarrow$
\end{column}
\begin{column}{5cm}
\footnotesize
\begin{alltt}
unsafe (p1 p2)
\{ PC[p1] = \textcolor{magenta}{L1} && PC[p2] = \textcolor{magenta}{L1} \}

transition crit (p)
requires \{ PC[p] = \textcolor{magenta}{L1} \}
\{
    PC[p] = \textcolor{green}{L2}
\}
\end{alltt}
\end{column}
\end{columns}


  
\end{frame}


\begin{frame}[fragile]{Formules logiques}

 Garde de transition sous cubicle : 
  
\begin{verbatim}
PC[x] = L4
&& forall_other y . (B[y] <> False || W[y] <> False)
\end{verbatim}
$\rightarrow$ Conjonction de littéraux et de DNF universellement quantifiées 

\medskip

Formules en \texttt{algony} :
\textcolor{blue}{\texttt{(a || b) \&\& (c || d)}} \\
$\rightarrow$ implique la mise en DNF et l'explosion en plusieurs
transitions dont les gardes sont les conjonctions (sauf DNF quantifiées) : 

\medskip

$t1\{a \wedge c\}, t2\{a \wedge d\}, t3\{b \wedge c\}, t4\{b \wedge d\}$

\end{frame}


\begin{frame}[fragile]{Les quantificateurs}

 Traduction du \texttt{forall\_other} $\rightarrow$ triviale (mise en DNF)

\medskip

Traduction du \texttt{exists\_other} :
n'existe pas dans cubicle

\medskip
Correspondance sémantique avec les \textcolor{blue}{paramètres de transitions} : 
\begin{verbatim}
await exists_other y . T[y] = true && T[x] = true


transition await (x y)
requires {T[y] = true && T[x] = true}
{...}
\end{verbatim}

\end{frame}


\begin{frame}{}

\begin{center}
\LARGE DEMO
\end{center}
  
\end{frame}


\begin{frame}{Perspectives}
\begin{itemize}
\item Exécution de code Algony par un interpréteur
\item Détection des interblocages
\item Prouver la correction de la traduction
\end{itemize}  
\end{frame}

\begin{frame}{Conclusion}

\begin{itemize}
  \item Possibilité d'écrire des algorithmes concurrents et de les
    vérifier avec Cubicle
  \item Compilateur d'Algony vers Cubicle et outil graphique\\
        $\rightarrow$ 1700 lignes de code OCaml
  \item Initation à la recherche, à la vérification de programme et au Model Checking
\end{itemize}

\end{frame}

\begin{frame}{}

\begin{center}
\LARGE Des questions ?
\end{center}
  
\end{frame}

\end{document}





# Local Variables:
# compile-command: "rubber -d --inplace slides.tex"
# End:
